agree\_on($T$;$x$.$P$($x$))($L_{1}$,$L_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\parallel$$L_{1}$$\parallel$ $=$ $\parallel$$L_{2}$$\parallel$ \& ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$}}$. $P$($L_{1}$[$i$]) $\vee$ $P$($L_{2}$[$i$]) $\Rightarrow$ $L_{1}$[$i$] $=$ $L_{2}$[$i$])